import GlimpseOfLean.Library.Basic
open Set

namespace ClassicalPropositionalLogic

/- 让我们尝试实现一种经典命题逻辑语言。

注意这里还有用于直觉主义逻辑的版本：
`IntuitionisticPropositionalLogic.lean`
-/

def Variable : Type := ℕ

/- 我们定义命题公式和一些符号。 -/

inductive Formula : Type where
  | var : Variable → Formula
  | bot : Formula
  | conj : Formula → Formula → Formula
  | disj : Formula → Formula → Formula
  | impl : Formula → Formula → Formula

open Formula
local notation:max (priority := high) "#" x:max => var x
local infix:30 (priority := high) " || " => disj
local infix:35 (priority := high) " && " => conj
local infix:28 (priority := high) " ⇒ " => impl
local notation (priority := high) "⊥" => bot

def neg (A : Formula) : Formula := A ⇒ ⊥
local notation:(max+2) (priority := high) "~" x:max => neg x
def top : Formula := ~⊥
local notation (priority := high) "⊤" => top
def equiv (A B : Formula) : Formula := (A ⇒ B) && (B ⇒ A)
local infix:29 (priority := high) " ⇔ " => equiv

/- 让我们定义相对于赋值的真值，即经典有效性 -/

@[simp]
def IsTrue (φ : Variable → Prop) : Formula → Prop
  | ⊥      => False
  | # P    => φ P
  | A || B => IsTrue φ A ∨ IsTrue φ B
  | A && B => IsTrue φ A ∧ IsTrue φ B
  | A ⇒ B => IsTrue φ A → IsTrue φ B

def Satisfies (φ : Variable → Prop) (Γ : Set Formula) : Prop := ∀ {A}, A ∈ Γ → IsTrue φ A
def Models (Γ : Set Formula) (A : Formula) : Prop := ∀ {φ}, Satisfies φ Γ → IsTrue φ A
local infix:27 (priority := high) " ⊨ " => Models
def Valid (A : Formula) : Prop := ∅ ⊨ A

/- 以下是有效性的一些基本性质。

  策略 `simp` 会自动简化用 `@[simp]` 标记的定义，并使用
  用 `@[simp]` 标记的定理进行重写。 -/

variable {φ : Variable → Prop} {A B : Formula}
@[simp] lemma isTrue_neg : IsTrue φ ~A ↔ ¬ IsTrue φ A := by simp [neg]

@[simp] lemma isTrue_top : IsTrue φ ⊤ := by
  -- sorry
  simp [top]
  -- sorry

@[simp] lemma isTrue_equiv : IsTrue φ (A ⇔ B) ↔ (IsTrue φ A ↔ IsTrue φ B) := by
  -- sorry
  simp [equiv]
  tauto
  -- sorry

/- 作为练习，让我们使用（经典逻辑）证明双重否定消除原理。
  `by_contra h` 可能对反证法证明有用。 -/

example : Valid (~~A ⇔ A) := by
  -- sorry
  intros φ _
  simp
  -- sorry

/- 我们经常需要向集合中添加元素。这通过 `insert` 函数完成：
`insert A Γ` 表示 `Γ ∪ {A}`。 -/

@[simp] lemma satisfies_insert_iff : Satisfies φ (insert A Γ) ↔ IsTrue φ A ∧ Satisfies φ Γ := by
  simp [Satisfies]

/- 让我们定义相对于经典逻辑的可证性。 -/
section
set_option hygiene false -- 这是允许记号中前向引用的技巧性方法
local infix:27 " ⊢ " => ProvableFrom

/- `Γ ⊢ A` 是存在一个结论为 `A` 且假设来自 `Γ` 的证明树的谓词。
  这是经典逻辑自然演绎的典型规则列表。 -/
inductive ProvableFrom : Set Formula → Formula → Prop
  | ax    : ∀ {Γ A},   A ∈ Γ   → Γ ⊢ A
  | impI  : ∀ {Γ A B},  insert A Γ ⊢ B                → Γ ⊢ A ⇒ B
  | impE  : ∀ {Γ A B},           Γ ⊢ (A ⇒ B) → Γ ⊢ A  → Γ ⊢ B
  | andI  : ∀ {Γ A B},           Γ ⊢ A       → Γ ⊢ B  → Γ ⊢ A && B
  | andE1 : ∀ {Γ A B},           Γ ⊢ A && B           → Γ ⊢ A
  | andE2 : ∀ {Γ A B},           Γ ⊢ A && B           → Γ ⊢ B
  | orI1  : ∀ {Γ A B},           Γ ⊢ A                → Γ ⊢ A || B
  | orI2  : ∀ {Γ A B},           Γ ⊢ B                → Γ ⊢ A || B
  | orE   : ∀ {Γ A B C}, Γ ⊢ A || B → insert A Γ ⊢ C → insert B Γ ⊢ C → Γ ⊢ C
  | botC  : ∀ {Γ A},   insert ~A Γ ⊢ ⊥                → Γ ⊢ A

end

local infix:27 (priority := high) " ⊢ " => ProvableFrom

/- 如果公式可以从空假设集合中证明，则称该公式是可证的。 -/
def Provable (A : Formula) := ∅ ⊢ A

export ProvableFrom (ax impI impE botC andI andE1 andE2 orI1 orI2 orE)
variable {Γ Δ : Set Formula}

/- 我们定义一个简单的策略 `apply_ax` 来使用 `ax` 规则证明某些东西。 -/
syntax "solve_mem" : tactic
syntax "apply_ax" : tactic
macro_rules
  | `(tactic| solve_mem) =>
    `(tactic| first | apply mem_singleton | apply mem_insert |
                      apply mem_insert_of_mem; solve_mem
                    | fail "tactic \'apply_ax\' failed")
  | `(tactic| apply_ax)  => `(tactic| { apply ax; solve_mem })

/- 要熟悉证明系统，让我们证明以下内容。
  你可以使用前几行定义的 `apply_ax` 策略，它证明使用 `ax` 规则可证的目标。
  或者你可以手动完成，使用以下关于 insert 的引理。
```
  mem_singleton x : x ∈ {x}
  mem_insert x s : x ∈ insert x s
  mem_insert_of_mem y : x ∈ s → x ∈ insert y s
```
-/

-- Let’s first see an example using the `apply_ax` tactic
example : {A, B} ⊢ A && B := by
  apply andI
  apply_ax
  apply_ax

-- 同样的内容，一次性手动完成。
example : {A, B} ⊢ A && B := by
  exact andI (ax (mem_insert _ _)) (ax (mem_insert_of_mem _ (mem_singleton _)))


example : Provable (~~A ⇔ A) := by
  -- sorry
  apply andI
  · apply impI
    apply botC
    apply impE _ (by apply_ax)
    apply_ax
  · apply impI
    apply impI
    apply impE (by apply_ax)
    apply_ax
  -- sorry

/- 可选练习：证明排中律。 -/
example : Provable (A || ~A) := by
  -- sorry
  apply botC
  apply impE (by apply_ax)
  apply orI2
  apply impI
  apply impE (by apply_ax)
  apply orI1 (by apply_ax)
  -- sorry

/- 可选练习：证明德摩根定律之一。
  如果你想说公理 `impE` 的参数 `A` 应该是 `X && Y`，
  你可以使用 `impE (A := X && Y)` 来做到这一点 -/
example : Provable (~(A && B) ⇔ ~A || ~B) := by
  -- sorry
  apply andI
  · apply impI
    apply botC
    apply impE (A := A && B) (by apply_ax)
    apply andI
    · apply botC
      apply impE (A := _ || _) (by apply_ax)
      apply orI1 (by apply_ax)
    · apply botC
      apply impE (A := _ || _) (by apply_ax)
      apply orI2 (by apply_ax)
  · apply impI
    apply impI
    apply orE (by apply_ax)
    · apply impE (by apply_ax)
      apply andE1 (by apply_ax)
    · apply impE (by apply_ax)
      apply andE2 (by apply_ax)
  -- sorry

/- 你可以使用对 `h` 的 `induction` 来证明以下内容。你需要告诉 Lean 你想使用 `induction h generalizing Δ` 同时对所有 `Δ` 证明它。Lean 会将创建的假设标记为不可访问的（用 † 标记），如果你没有明确地命名它们。
  你可以使用例如 `rename_i ih` 或 `rename_i A B h ih` 来命名最后的不可访问变量。或者你可以使用 `case impI ih => <proof>` 证明特定情况。你可能需要使用引理 `insert_subset_insert : s ⊆ t → insert x s ⊆ insert x t`。 -/
lemma weakening (h : Γ ⊢ A) (h2 : Γ ⊆ Δ) : Δ ⊢ A := by
  -- sorry
  induction h generalizing Δ
  case ax => apply ax; solve_by_elim
  case impI ih => apply impI; solve_by_elim [insert_subset_insert]
  case impE ih₁ ih₂ => apply impE <;> solve_by_elim
  case andI ih₁ ih₂ => apply andI <;> solve_by_elim
  case andE1 ih => apply andE1 <;> solve_by_elim
  case andE2 ih => apply andE2 <;> solve_by_elim
  case orI1 ih => apply orI1; solve_by_elim
  case orI2 ih => apply orI2; solve_by_elim
  case orE ih₁ ih₂ ih₃ => apply orE <;> solve_by_elim [insert_subset_insert]
  case botC ih => apply botC; solve_by_elim [insert_subset_insert]
  -- sorry

/- 使用 `apply?` 策略找到陈述 `Γ ⊆ insert x Γ` 的引理。你可以点击右侧面板中的蓝色建议来自动应用建议。 -/

lemma ProvableFrom.insert (h : Γ ⊢ A) : insert B Γ ⊢ A := by
  -- sorry
  apply weakening h
  -- 在这里使用 `apply?`
  exact subset_insert B Γ
  -- sorry

/- 现在证明演绎定理很容易。 -/
lemma deduction_theorem (h : Γ ⊢ A) : insert (A ⇒ B) Γ ⊢ B := by
  -- sorry
  apply impE (ax $ mem_insert _ _)
  exact h.insert
  -- sorry

lemma Provable.mp (h1 : Provable (A ⇒ B)) (h2 : Γ ⊢ A) : Γ ⊢ B := by
  -- sorry
  apply impE _ h2
  apply weakening h1
  -- apply?
  exact empty_subset Γ
  -- sorry

/-- 你需要使用策略 `left` 和 `right` 来证明析取，并且使用
  策略 `cases h`（如果 `h` 是析取）来进行情况区分。 -/
theorem soundness_theorem (h : Γ ⊢ A) : Γ ⊨ A := by
  -- sorry
  induction h <;> intros φ hφ
  solve_by_elim
  case impI ih => intro hA; apply ih; simp [*]
  case impE ih₁ ih₂ => exact ih₁ hφ (ih₂ hφ)
  case botC ih => by_contra hA; apply ih (satisfies_insert_iff.mpr ⟨by exact hA, hφ⟩)
  case andI ih₁ ih₂ => exact ⟨ih₁ hφ, ih₂ hφ⟩
  case andE1 ih => exact (ih hφ).1
  case andE2 ih => exact (ih hφ).2
  case orI1 ih => exact .inl (ih hφ)
  case orI2 ih => exact .inr (ih hφ)
  case orE ih₁ ih₂ ih₃ => refine (ih₁ hφ).elim (fun hA => ih₂ ?_) (fun hB => ih₃ ?_) <;> simp [*]
  -- sorry

theorem valid_of_provable (h : Provable A) : Valid A := by
  -- sorry
  exact soundness_theorem h
  -- sorry

/-
  如果你愿意，你现在可以尝试一些这些较长的项目。

  1. 证明完备性：如果一个公式是有效的，那么它是可证的
  以下是此证明的一种可能策略：
  * 如果一个公式是有效的，那么它的否定范式 (NNF) 也是有效的；
  * 如果 NNF 中的公式是有效的，那么它的合取范式 (CNF) 也是有效的；
  * 如果 CNF 中的公式是有效的，那么它在语法上是有效的：
      它的所有子句都包含某个 `A` 的 `A` 和 `¬ A`（或包含 `⊤`）；
  * 如果 CNF 中的公式在语法上是有效的，那么它是可证的；
  * 如果 NNF 中公式的 CNF 是可证的，那么公式本身也是可证的。
  * 如果公式的 NNF 是可证的，那么公式本身也是可证的。

  2. 为命题逻辑定义 Gentzen 的序列演算，并证明这产生了
  相同的可证性。
-/

end ClassicalPropositionalLogic
